es:ES, e:E, l:IdLnk, L:E List. rcvs from e on l = L  Prop 

latex

Definitions	x:A. B(x), t  T, Prop, rcvs from e on l = L, A & B, P  Q, P & Q, P  Q, P  Q
Lemmas	es-E wf, iff wf, l member wf, assert wf, es-isrcv wf, IdLnk wf, es-lnk wf, es-sender wf, l before wf, es-locl wf, event system wf